Our type system builds upon the one in~\cite{DBLP:journals/entcs/YoshidaV07},
extending it so as to account for disciplined runtime adaptation.
%\cite{DBLP:conf/ppdp/GarraldaCD06}.
%As mentioned in the Introduction, a 
A
main criteria in the design of our type discipline is \emph{conservativity}:
we would like to enforce both structured communication and disciplined adaptation by preserving standard models of session types as much as possible. \done\todo[B31.]{Fixed, pls check.} 

\subsection{Type Syntax}
We now define our type syntax, which is rather standard.
%Our type syntax is as follows: %defined next, contains the usual session types constructs: %---we exclude recursive types.

%As such, the type syntax is divided into three categories: \emph{basic types}, which  handle expressions; 
%\emph{pre-session types} describing a channel's ability for sending/receiving messages and offering/selecting be\-hav\-iors; 
%\emph{session types} representing well-formed session-typed be\-hav\-ior. %; and
%\emph{channel types}, which can be a session type or a \emph{used session}~$\bot$. %this will be made clear later on).

%We extend the judgments of~\cite{DBLP:conf/ppdp/GarraldaCD06} with an \emph{interface} $\INT$---the collection of all session types declared in a given process. 
%
%Formally, we have:

%\end{document}
 
\begin{definition}[Types]\label{d:types}
The syntax of 
 \emph{basic types} (ranged over $\capab, \sigma,   \ldots$) %, \emph{pre-session types} ($\zeta$), 
 and
 %(qualified) 
 \emph{session types} (ranged over $\ST, \beta, \ldots$)
% and \emph{channel types} ($\omega$) 
is given in Table~\ref{tab:types}.
\end{definition}

\begin{table}[t!]
\textsc{Types}
$$
\begin{array}{lclr}
\capab, \sigma & ::= & \mathsf{int} \sepr \mathsf{bool} \sepr \dots ~~~& \text{basic types}\\

\alpha, \beta &::=  &  !(\widetilde{\capab}).\alpha \sepr ?(\widetilde{\capab}).\alpha & \text{send, receive} \\ 
		& \sepr &  !(\beta).\alpha \sepr ?(\beta).\alpha & \text{throw, catch} \\ 
		& \sepr &  \&\{n_1:\alpha_1, \dots,  n_m:\ST_m \}  \quad &  \text{branch} \\
		& \sepr &  \oplus\{n_1:\alpha_1, \dots , n_m:\ST_m \}  &  \text{select} \vspace{0.5mm} \\
		& \sepr &  \epsilon \!\!\!\!\!\!& \text{closed session}
\end{array}
$$
\textsc{Environments}
$$
\begin{array}{lclr}
		\qua & ::= &  \qual \sepr \quau  & \text{type qualifiers} \vspace{0.5mm} \\
%\INT &::= &  \emptyset \sepr \INT, \langle a: \ST, h \rangle & \text{interface} \\
\ActS & ::= &  \emptyset \sepr \ActS , k:\ST \sepr \ActS ,  [k:\ST]  & \text{typing with active sessions}\\
\Gamma &::= &  \emptyset \sepr \Gamma, e:\capab \sepr \Gamma, a:\langle \ST_\qua , \overline{\ST}_\qua \rangle \quad& \text{first-order environment}\\
\Theta &::= &  \emptyset \sepr  \Theta,\mathsf{X}:\INT \sepr \Theta,l:\INT     \quad& \text{higher-order environment}
\end{array}
$$  
\caption{Types and Typing Environments. Interfaces $\INT$ are formally introduced in Definition~\ref{d:interf}.}\label{tab:types}
\end{table}



% We use $t, t', \ldots$ to range over \emph{type variables}; also, we 
% require recursive types to be \emph{contractive}, i.e., not 
% containing a subexpression of the form $\mu t.\mu t_1.\cdots.\mu t_n.t$.
% Binder $\mu$ gives rises to standard notions of free/bound type variables; 
% $\mathsf{ftv}(\zeta)$ denotes the free type variables in $\zeta$.
% We consider session types modulo folding/unfolding of recursive types.
%\todo{contractive types?}
We recall the intuitive meaning of session types. 
We write $\til{\tau}$ to denote a sequence of base types $\tau_1, \ldots, \tau_n$.
Type $?(\til{\capab}).\ST$ (resp. $?(\beta).\ST$) abstracts the behavior of a channel 
which receives values of types $\til{\capab}$ (resp. a channel of type $\beta$) 
and continues as $\ST$ afterwards.
Complementarily, type $!(\til{\capab}).\ST$ (resp. $!(\beta).\ST$) represents the behavior
of a channel which sends values (resp. a channel)  and that continues as $\ST$ afterwards.
Type $\&\{n_1:\alpha_1, \dots,  n_m:\ST_m \}$ describes a branching behavior, or external choice, along a channel:
it offers $m$ behaviors, and if the $j$-th alternative is selected then it behaves as described by type $\ST_j$ ($1 \leq j \leq m$).
In turn, type $\oplus\{n_1:\alpha_1, \dots , n_m:\ST_m \}$ describes the behavior of a channel which 
may select a single behavior among  $\alpha_1, \ldots, \alpha_m$. This is an internal choice, which continues as $\ST_j$ afterwards.
Finally, type $\epsilon$ represents a channel with no communication behavior. 
We now introduce the central notion of  \emph{duality} for (session) types.


\begin{definition}[Duality]\label{d:dual}
Given a session type $\ST$, 
its \emph{dual}
(noted $\overline{\ST}$) is inductively defined in Table~\ref{tab:dual}.
\begin{table}[t]
$$
\begin{array}{rcl}
 \overline{\epsilon} & =  & \epsilon\\
 \overline{!(\til{\capab}).\ST} & =  & ?(\til{\capab}).\overline{\ST} \\
 \overline{?(\til{\capab}).\ST} & =  & !(\til{\capab}).\overline{\ST} \\
 \overline{!(\beta).\ST} & =  & ?(\beta).\overline{\ST} \\
 \overline{?(\beta).\ST} & =  & !(\beta).\overline{\ST} \\
% \overline{t} &\!\!=\! & t \\
 %\overline{\mu t.\ST} &\!\!=\! & \mu t.\overline{\ST}\\
 \overline{\&\{n_1:\ST_1 , \ldots , n_m:\ST_m \}} &\!\!=\! & \oplus\{n_1:\overline{\ST_1} , \ldots , n_m:\overline{\ST_m} \}\\
 \overline{ \oplus\{n_1:\ST_1 , \ldots , n_m:\ST_m \}} &\!\!=\!& \&\{n_1:\overline{\ST_1} , \ldots , n_m:\overline{\ST_m} \}
\end{array}
$$ %\vspace{-4mm}
\caption{Dual of session types}\label{tab:dual}
\end{table}
\end{definition}

%Before introducing our notion of typing environment
\done\todo[B32.]{Fixed, pls check.}
Our typing judgments generalize usual notions with an  \emph{interface}~$\INT$ (see Def.~\ref{d:interf}). 
Based on the syntactic occurrences of prefixes $\nopenr{a}{x}$, $\nopena{a}{x}$, and $\repopen{a}{x}$,
the interface of a process describes the (possibly persistent) services appearing in it.
Thus, intuitively, the interface of a process gives an ``upper bound'' on the services that a process may execute.
Formally, we have:
%We now formally define the concept of interface, motivated above.
%Recall that we use $j,h,\ldots$ to range over 
%$\mathbb{N}_0$.
%integers.
%\done\todo[B10.]{Added a note concerning $h$, missing some other two issues.}

%\begin{definition}[Interfaces OLD]\label{d:interfold}
%An \emph{interface} $\INT$ is a set of pairs  $\langle a: \ST, h\rangle$ where 
%$a$ is name, $\ST$ is a session type, and either $h> 0$ or $h = \infty$.
%The extension of an interface $\INT$ with a pair $\langle a: \ST, h\rangle$, written $\INT \addelta \inter{a}{\alpha}{h}$,
%is defined as follows:
%$$
%\INT \addelta \inter{a}{\alpha}{h} \triangleq
%\begin{cases}
%\INT' \cup \{\inter{a}{\ST}{h + j} \} & \text{if } \exists\INT'. \,  \INT = \INT' \cup \{\inter{a}{\ST}{j} \}	\\
%\INT \cup \{\inter{a}{\ST}{h}\} & \text{otherwise} 
%\end{cases}
%$$
%Given $\INT$, we write $\INT_\quau$ 
%and $\INT_\qual$
%to denote sets $\{ \inter{a}{\ST}{h} \,|\, \inter{a}{\ST}{h} \in \INT \land h = \infty\}$ and
%$\INT - \INT_\quau$, respectively. \\
%Moreover, we write $\INT \unres$ 
%to denote the set $\{ \inter{a}{\alpha}{\infty} \mid   \inter{a}{\alpha}{h} \in \INT_\qual \} \cup \INT_\quau$.
%%Finally we define the  function $$\unres(\INT) \triangleq \{ \inter{a}{\alpha}{\infty} \mid   \inter{a}{\alpha}{h} \in \INT \}$$
%\end{definition}


\begin{definition}[Interfaces]\label{d:interf}
We define an \emph{interface} as the multiset whose underlying set of elements 
$\mathrm{Int}$ contains 
assignments from names to session types which are qualified (cf. Table~\ref{tab:types}).
More precisely: $$\mathrm{Int} = \{ \qua\,a{:}\ST ~|~ \qua \in \{\qual, \quau\}, 
\text{$a$ is a name, and $\ST$ is a session type}\}$$
We use $\INT, \INT', \ldots$ to range over interfaces.
We sometimes write $\#_\INT(a) = h$ to mean that element $a$ occurs $h$ times in $\INT$.
\end{definition}

%
%OLD TEXT: We recall that $\infty + 1 = \infty$.
%Intuitively, interfaces capture the services declared in a process\todo[C8.]{Clarify intuitions for interfaces?} (i.e., an assignment from names to session types)
%together with
%the number of times such a service is declared ($j>0$ if a type is linear; $\infty$ otherwise).
%In $\INT$, services are recorded at most once; several occurrences of the same linear service are captured
%by the second component of the pair.   
%We sometimes write $\INT \addelta a:\ST_\qual$ 
%and  $\INT \addelta a:\ST_\quau$
%to stand 
%for $\INT \addelta\{\inter{a}{\ST}{1} \}$ and 
%$\INT \addelta \{\inter{a}{\ST}{\infty} \}$, respectively.
%The extension of $\addelta$ from single pairs $\inter{a}{\ST}{h}$ 
%to interfaces, denoted $\INT_1 \addelta \INT_2$, is as expected. 


%NEW TEXT: 
%Intuitively, interfaces capture the services declared in a process, including their possibly persistent nature.
Observe how several occurrences of the same service declaration are captured by the multiset nature of interfaces.
The union of two interfaces $\INT_1$ and $\INT_2$ is essentially the union of their underlying multisets.
We sometimes write $\INT \addelta a:\ST_\qual$ 
and  $\INT \addelta a:\ST_\quau$
to stand 
for $\INT \addelta\{\qual\,a{:}\ST\}$ and 
$\INT \addelta \{\quau\,a{:}\ST\}$, respectively.

\begin{newnotation}[Interfaces]\label{n:interf}
We write $\INT_\qual$ (resp. $\INT_\quau$) to denote the subset of $\INT$ involving
only assignments qualified with $\qual$ (resp. $\quau$). 
Moreover, we write $\INT \unres$ to denote the ``persistent promotion'' of $\INT$. Formally, 
$\INT \unres = \INT \setminus \INT_\qual \addelta \{\quau\,a{:}\ST \mid   \qual\,a{:}\ST \in \INT_\qual \}$.
%Furthermore, we write $\INT  \intpr \INT'$  to denote that interface $\INT$ is included in $\INT'$.
\end{newnotation}

It is useful to relate different interfaces. % which only differ in the linear services they contain.
This is the intention of the relation $\intpr$ over interfaces, defined next.
%
%\begin{definition}[OLD Interface Ordering] \label{d:intpre}Given interfaces $\INT$ and $\INT'$, we write 
%$\INT  \intpr \INT'$ iff 
%\begin{enumerate}[1.]
%\item $\INT_\qual \subseteq \INT'_\qual$, where $\subseteq$ is the usual ordering on multisets; 
%\item $\forall (\quau\,a{:}\ST) \in \INT_\quau $  then 
%$ (\quau \, a{:}\ST) \in \INT'_\quau $.
%\done\todo[B11.]{We need to understand this comment.}
%\end{enumerate}
%\end{definition}
%
\begin{definition}[Interface Ordering] \label{d:intpre}Given interfaces $\INT$ and $\INT'$, we write 
$\INT  \intpr \INT'$ iff 
\begin{enumerate}[1.]
\item 
One of the following holds:
\begin{enumerate}[(a)]
\item $\INT_\qual \subseteq \INT'_\qual$, where $\subseteq$ is the usual ordering on multisets, or 
\item $\forall (\qual\,a{:}\ST) \in \INT_\qual \setminus \INT_\qual'$ then  $(\quau\,a{:}\ST) \in \INT'_\quau$
\end{enumerate}
\item $\forall (\quau\,a{:}\ST) \in \INT_\quau $  then $ (\quau \, a{:}\ST) \in \INT'_\quau $.
\end{enumerate}
Interface equality is defined as: $\INT_1 = \INT_2$ iff  $\INT_1 \intpr \INT_2$ and $\INT_2 \intpr \INT_1$
\end{definition}

In the light of the previous definitions, we may state:

\begin{lemma}
Relation \intpr is a preorder.
\end{lemma}
%
%As we will see, our typing system will be parametric on the definition of \intpr.
%Alternative definitions for this relation are discussed in Sect.~\ref{sec:int}.
\done\todo[B12.]{We need to understand this comment.}

\subsection{Environments, Judgments and Typing Rules}
The typing environments we rely on are defined in the lower part of Table~\ref{tab:types}.
In addition to interfaces $\INT$, we consider typings $\ActS$ and environments $\Gamma$ and $\Theta$.

%In session type disciplines, 
Typing $\ActS$ is commonly used to collect
assignments from channels to session types; as such, it describes
currently active sessions. 
In our discipline, 
%Unlike usual disciplines, however, 
in $\ActS$ we also include \emph{bracketed assignments}, denoted $[\kappa^p:\ST]$,
which represent active but restricted sessions. 
As we discuss below, bracketed assignments arise in the typing of %channel 
restriction, 
and are key to keep a precise count of the active sessions in a given located process. \done\todo[A8.]{Slightly rephrase to emphasize on the need of correctness of counting.} 
We write $dom(\ActS)$ to denote the set $\{ k^p \mid k^p:\ST \in \ActS \lor [k^p:\ST] \in \ActS\}$.
We write $\ActS , k:\ST $ and $\ActS , [k:\ST] $ where $k \not\in dom(\ActS)$. % (and similarly for the other environments).


$\Gamma$ is a first-order environment which maps expressions to basic types
and names to pairs of \emph{qualified} session types.
In  the interface, a session type is qualified with 
`$\quau$' if it is associated to a persistent service; otherwise, it is qualified with 
`$\qual$'.
%While $\qual$ is used for those session types %to be used %just once, 
%associated to linear services, we use 
%$\quau$ to qualify  session types %intended to feature a persistent behavior.
%associated to persistent services.\todo[B13.]{I have used the linear/persistent terminology introduced before. Please check.}

The higher-order environment $\Theta$ 
collects assignments of process variables and locations to interfaces. 
While the former kind of assignments is relevant to update processes, the latter concern located processes.
As we explain next, by relying on the combination of these two pieces of information the type system ensures that
runtime adaptation actions preserve the behavioral interfaces of a process.
%\jp{The following is a bit strange for locations are also in $\T$; I would write $vdom(\T)$ if you only care about variables.} \todo{
We write $vdom(\Theta)= \{ \mathsf{X} \mid \mathsf{X}:\INT \in \Theta \}$ to denote the variables in the domain of $\Theta$.
%}
Given these environments, a \emph{type judgment} is  of form
$$\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}} $$ 
meaning that, under environments $\Gamma$ and $\Theta$, 
process $P$ has active sessions declared in $\ActS$ and interface 
$\INT$.\done\todo[B14.]{I changed the notation for judgments, please check consistency.} We then have:

\begin{definition}%[Well-typed process]
A process is well-typed if it can be typed using the rules in Tables~\ref{tab:ts} and~\ref{tab:session}.


\begin{table}[th!]
$$
\begin{array}{c}
% \mathrm{\textsc{Comp}}~~~\component{a}{P} \arro{~\component{a}{P}~}  \star
\inferrule*[left=\rulename{t:Exp}]{ }{\Gamma \vdash e:\capab}{}\done\todo[B34.]{We have single typing rule per line, please check.} 
\vspace{2mm} \\
\inferrule*[left=\rulename{t:NVar}]{ }{\Gamma, x:\capab \vdash x:\capab} 
\vspace{2mm} \\
\inferrule*[left=\rulename{t:Nil}]{ }{\judgebis{\env{\Gamma}{\Theta}}{\nil}{\type{\emptyset}{\emptyset}}}
\vspace{2mm} \\
\inferrule*[left=\rulename{t:LocEnv}]{ }{\Theta, l:\INT \vdash l:\INT} 
\vspace{2mm} \\
\inferrule*[left=\rulename{t:PVar}]{ }{\Gamma; \Theta,\mathsf{X}:\INT \vdash \mathsf{X}:\type{\emptyset}{\INT}}
\vspace{2mm} \\
\inferrule*[left=\rulename{t:Accept}]{\Gamma \vdash a: \langle \ST_\qual , \overline{\ST}_\qual  \rangle \qquad \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, x:\ST}{\,\INT}}}{\judgebis{\env{\Gamma}{\Theta}}{\nopena{a}{x}.P}{ \type{\ActS}{\,\INT \addelta a: \ST_\qual}}}
\vspace{2mm} \\
\inferrule*[left=\rulename{t:RepAccept}]
 {\Gamma \vdash a: \langle \ST_\quau , \overline{\ST}_\qual  \rangle \qquad \judgebis{\env{\Gamma}{\Theta}}{P}{\type{x:\ST}{\,\INT}} 
}{\judgebis{\env{\Gamma}{\Theta}}{\repopen{a}{x}.P}{ \type{\emptyset}{\INT\unres \addelta \, a: \ST_\quau}}}
\vspace{2mm} \\
\inferrule*[left=\rulename{t:Request}]
 {
\Gamma \vdash a: \langle \ST_\qua , \overline{\ST}_\qual \rangle \qquad
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, x:\overline{\ST }}{\,\INT}} 
}{\judgebis{\env{\Gamma}{\Theta}}{\nopenr{a}{x}.P}{ \type{\ActS}{\,\INT \addelta a: \overline{\ST}_\qual }}} 
\vspace{2mm} \\
\inferrule*[left=\rulename{t:Clo}]
 {\judgebis{\env{\Gamma}{\Theta}}{ P}{\type{\ActS}{\INT}} \qquad k\notin \dom{\ActS} }{\judgebis{\env{\Gamma}{\Theta}}{ \close{k}.P}{ \type{\ActS, k:\epsilon}{ \INT}}}
\vspace{2mm} \\
\inferrule*[left=\rulename{t:Loc} ]
 {
       \Theta \vdash l:\INT \qquad \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT' } } \qquad  h = | \ActS |  \qquad \INT' \intpr \INT
 }{\judgebis{\env{\Gamma}{\Theta}}{\component{l}{h}{\INT}{P} }{ \type{\ActS}{\INT' }}}
\vspace{2mm} \\
\inferrule*[left=\rulename{t:Adapt} ] 
{\Theta \vdash l:\INT  \qquad  \judgebis{\env{\Gamma}{\Theta,\mathsf{X}:{\INT}}}{P}{\type{\emptyset}{ \INT' }}}{\judgebis{\env{\Gamma}{\Theta}}{\adapt{l}{P}{X}}{\type{\emptyset}{ \emptyset}}}
\vspace{2mm} \\
\inferrule*[left=\rulename{t:CRes}]
 {\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS, \cha^-:\ST, \cha^+:\overline{\ST} }{ \INT}}}{\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{P}}{\type{\ActS, [\cha^-:\ST], [\cha^+:\overline{\ST}]}{ \INT}}}
\vspace{2mm} \\
\inferrule*[left=\rulename{t:Par}]
 {
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_1}{ \INT_1}} \qquad
 \judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS_2}{ \INT_2}}
 }{\judgebis{\env{\Gamma}{\Theta}}{P \para Q}{\type{\ActS_1 \cup \ActS_2}{\INT_1 \addelta \INT_2}}}
 \end{array}
 $$
\caption{Well-typed processes (I)} \label{tab:ts}
\end{table}
\end{definition}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\begin{table}[!t]
%$$
%\begin{array}{cr}
%\cfrac{}{\Gamma \vdash e:\capab} \qquad 
%\cfrac{}{\Gamma, x:\capab \vdash x:\capab}  \qquad
%\cfrac{}{\judgebis{\env{\Gamma}{\Theta}}{\nil}{\type{\emptyset}{\emptyset}}} 
% & \rulename{t:Exp},  \rulename{t:NVar}, \rulename{t:Nil} \\
%
%\cfrac{}{\Theta, l:\INT \vdash l:\INT}
%\quad \cfrac{}{\Gamma; \Theta,\mathsf{X}:\INT \vdash \mathsf{X}:\type{\emptyset}{\INT}}
%&    \rulename{t:LocEnv},  \rulename{t:PVar}   \vspace{2mm}\\
%
% \cfrac{
%\Gamma \vdash a: \langle \ST_\qual , \overline{\ST_\qual } \rangle \qquad
%\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, x:\ST}{\,\INT}} 
%}{\judgebis{\env{\Gamma}{\Theta}}{\nopena{a}{x}.P}{ \type{\ActS}{\,\INT \addelta a: \ST_\qual}}} 
%& 
%\rulename{t:Accept} \vspace{2mm} 
%\\
%
% \cfrac{
%\Gamma \vdash a: \langle \ST_\quau , \overline{\ST_\qual } \rangle \qquad
%\judgebis{\env{\Gamma}{\Theta}}{P}{\type{x:\ST}{\,\INT}} 
%}{\judgebis{\env{\Gamma}{\Theta}}{\repopen{a}{x}.P}{ \type{\emptyset}{\INT\unres \addelta \, a: \ST_\quau}}} 
%& 
%\rulename{t:RepAccept} \vspace{2mm} 
%\\
%
%% \cfrac{
%%\Gamma \vdash a: \langle \ST_\quau , \overline{\ST_\qual } \rangle \quad
%%\judgebis{\env{\Gamma}{\Theta}}{P}{\type{x:\ST}{\,\todo{$\INT_\quau$}}} 
%%}{\judgebis{\env{\Gamma}{\Theta}}{\repopen{a}{x}.P}{ \type{\emptyset}{\INT_\quau \addelta \, a: \ST_\quau}}} 
%%& 
%%\rulename{t:RepAcceptProp} \vspace{2mm} 
%%\\
%
%\cfrac{
%\Gamma \vdash a: \langle \ST_\qua , \overline{\ST_\qual} \rangle \qquad
%\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, x:\overline{\ST }}{\,\INT}} 
%}{\judgebis{\env{\Gamma}{\Theta}}{\nopenr{a}{x}.P}{ \type{\ActS}{\,\INT \addelta a: \overline{\ST_\qual }}}} 
%& 
%\rulename{t:Request} \vspace{2mm} 
%\\
% \cfrac{\judgebis{\env{\Gamma}{\Theta}}{ P}{\type{\ActS}{\INT}} \qquad k\notin \dom{\ActS} }{\judgebis{\env{\Gamma}{\Theta}}{ \close{k}.P}{ \type{\ActS, k:\epsilon}{ \INT}}} & \rulename{t:Clo} \vspace{2mm} \\
%
%\cfrac{
%       \Theta \vdash l:\INT \qquad \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT' } } \qquad  h = | \ActS |  \qquad \INT' \intpr \INT
% }{\judgebis{\env{\Gamma}{\Theta}}{\component{l}{h}{\INT}{P} }{ \type{\ActS}{\INT' }}} &  \rulename{t:Loc}  \vspace{2mm}
%\\
%
%
%\cfrac{\Theta \vdash l:\INT  \qquad  \judgebis{\env{\Gamma}{\Theta,\mathsf{X}:{\INT}}}{P}{\type{\emptyset}{ \INT' }}}{\judgebis{\env{\Gamma}{\Theta}}{\adapt{l}{P}{X}}{\type{\emptyset}{ \emptyset}}} & \rulename{t:Adapt}  \vspace{2mm}
%
%\\
% 
%\cfrac{\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS, \cha^-:\ST, \cha^+:\overline{\ST} }{ \INT}}}{\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{P}}{\type{\ActS, [\cha^-:\ST], [\cha^+:\overline{\ST}]}{ \INT}}} 
%& \rulename{t:CRes} 
%\vspace{2mm}
%
%\\
%\cfrac{
%\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_1}{ \INT_1}} \qquad
% \judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS_2}{ \INT_2}}
% \qquad
% \INT = \INT_1 \addelta \INT_2}{\judgebis{\env{\Gamma}{\Theta}}{P \para Q}{\type{\ActS_1 \cup \ActS_2}{\INT}}} & \rulename{t:Par}  
%\end{array}
%$$
%\caption{Well-typed processes (I)} \label{tab:ts}
%\end{table}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{table}[th!]
$$
\begin{array}{c}
\inferrule*[left=\rulename{t:Thr}] 
{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\STT}{ \INT}}}{\judgebis{\env{\Gamma}{\Theta}}{\throw{k}{k'}.P}{\type{\ActS, k:!(\ST).\STT, k':\ST}{ \INT}}}
\vspace{2mm} \\
\inferrule*[left=\rulename{t:Cat}]
{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\STT, x:\ST}{\INT}}}{\judgebis{\env{\Gamma}{\Theta}}{\catch{k}{x}.P }{\type{\ActS, k:?(\ST).\STT}{ \INT}}}
\vspace{2mm} \\
\inferrule*[left=\rulename{t:In}]
{\judgebis{\env{\Gamma, \til{x}:\til{\capab}}{\Theta}}{P}{\type{\ActS, k:\ST}{\INT}}}{\judgebis{\env{\Gamma}{\Theta}}{\inC{k}{\til{x}}.P }{\type{\ActS, k:?(\til{\capab}).\ST}{ \INT}}}
\vspace{2mm} \\
\inferrule*[left=\rulename{t:Out}]
{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\ST}{ \INT}} \quad \Gamma \vdash \til{e}:\til{\capab}}{\judgebis{\env{\Gamma}{\Theta}}{\outC{k}{\til{e}}.P}{\type{\ActS, k:!(\til{\capab}).\ST}{ \INT}}}
\vspace{2mm} \\
\inferrule*[left=\rulename{t:Weak}] 
{\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS}{ \INT}  } \qquad \cha^+, \cha^- \notin dom(\ActS)}{\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{P}}{\type{\ActS}{ \INT }}}
\vspace{2mm} \\
\inferrule*[left=\rulename{t:If}]
 {
 \Gamma \vdash e:\mathsf{bool} \qquad
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}} \qquad
\judgebis{\env{\Gamma}{\Theta}}{Q}{\type{\ActS}{\INT}}
 }{\judgebis{\env{\Gamma}{\Theta}}{\ifte{e}{P}{Q}}{\type{\ActS}{\INT}}} 
\vspace{2mm} \\
\inferrule*[left=\rulename{t:Bra}] 
{
\judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{\ActS, k:\ST_1}{ \INT_1}} 
\quad 
\cdots
\quad
\judgebis{\env{\Gamma}{\Theta}}{P_m}{\type{\ActS, k:\ST_m}{ \INT_m}} \quad \INT = \INT_1 \uplus ...\uplus \INT_m
 }{\judgebis{\env{\Gamma}{\Theta}}{\branch{k}{n_1{:}P_1 \alte \cdots \alte  n_m{:}P_m}}{\type{ \ActS, k:\&\{n_1{:}\ST_1, \ldots, n_m{:}\ST_m \}}{\INT}}}
\vspace{2mm} \\
\inferrule*[left=\rulename{t:Sel}]
{
\judgebis{ \env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\ST_i}{ \INT}} \qquad 1 \leq i \leq m 
}{\judgebis{\env{\Gamma}{\Theta}}{\select{k}{n_i};P}{\type{\ActS, k:\oplus\{n_1:\ST_1, \ldots,  n_m:\ST_m \}}{\INT}}}
\end{array}
$$% \vspace{-4mm}
\caption{Well-typed processes (II)}\label{tab:session}
\end{table}




We comment on some %non standard 
rules in Table~\ref{tab:ts}.
Given a process which implements session type $\ST$  on channel $x$, 
rule \rulename{t:Accept} types a service on name~$a$. 
Observe how $x$ is removed from $\ActS$ whereas
 $\INT$ is appropriately extended with $a : \ST_\qual$. Rule \rulename{t:RepAccept} is the analogous of \rulename{t:Accept} for persistent services.
In that rule, observe how the linear services in  $\INT$ are ``promoted'' to persistent services via $\INT\unres$ (cf. Not.~\ref{n:interf}).
%\todo{
Non persistent services that appear in the context of a persistent service $a$ are meant to be executed %exactly 
at most
once for each instance of $a$. 
In fact, after promotion the declaration in $\Gamma$ for a non persistent service $b:\langle \ST_{\qual}, \overline{\ST}_{\qual} \rangle$ remains unchanged, but its entry in $\INT$ should be 
%$\inter{b}{\ST}{\infty}$, 
$\quau\,b{:}\ST$,
as we could now observe an unbounded number of executions of (non persistent) service $b$.
%}
%\jp{Cinzia, please check I didn't modified the intended meaning of your text.}
Given these typing rules, rule \rulename{t:Request} should be self-explanatory.

Rule~\rulename{t:CRes} types channel restriction. 
The main difference wrt usual typing rules for channel restriction (cf.~\cite{DBLP:journals/entcs/YoshidaV07}) is that 
restricted end-points are not removed from $\ActS$ but kept in bracketed form, as motivated earlier. 
Using typing $\ActS$,
we can have an exact count of open, possibly restricted, sessions in a process.
Rule~\rulename{t:Close} types the explicit session closure construct, extending 
$\ActS$ with a fresh channel which is assigned to an empty session type. 
This may be useful to understand why our typing rule for the inactive process (rule \rulename{t:Nil})
requires an empty typing $\Delta$.

%\jp{Far notare la nostra regola Rule \rulename{t:Nil} inizia da un $\Delta$ vuoto...}
Rule~\rulename{t:Loc} performs two checks to type located processes. First, the runtime annotation 
$h$ is computed by counting the assignments (standard and bracketed) declared in $\ActS$ (see~\ref{ap:count}). \done\todo[A9.]{This is extremely silly, but it is better to add the formal definition of $|\Delta|$}
Second, the rule checks that the interface of the located process is less  or equal (in the sense of $\intpr$, cf. Not.~\ref{n:interf}) than the
declared interface of the given location. 
Informally, this ensures that the process behavior does not ``exceed'' the expected behavior within the location.
It is worth observing how a typed located processes has the exact same typing and interface of its contained process:
this is how transparency of locations arises in typing.
Finally, rule \rulename{t:Adapt} types update processes. Observe how the interface associated to the process variable of the given 
 adaptation routine should match with the declared interfaces for the given location. 
However, for simplicity we establish no condition on the relation between $\INT$ (the expected interface) 
and $\INT'$ (the interface of the adaptation routine $P(\mathsf{X})$)
%---Sect.~\ref{sec:int} 
---in \S\,\ref{sec:recsub} we discuss an alternative, more stringent, formulation.
%\jp{Should we say something about $\INT'$?, yes but not here}
%This way, the rule guarantees that the process resulting from an update action has the declared interfaces. 

Having introduced our typing system, the following section defines and states its main properties.

%Rule \rulename{t:Par} puts processes in parallel. 
%Rules \rulename{t:PVar}  handle process  variables. 
%Rule \rulename{t:Weak} handles all those processes in which $\restr{c}{P} \equiv P$ holds, and 
%\rulename{t:CRes} types channel restriction. 
%While rules \rulename{t:Cat} and \rulename{t:Thr} handle delegation,
%rules \rulename{t:In}, \rulename{t:Out},  \rulename{t:If}, 
%\rulename{t:Bra},  and \rulename{t:Sel} are standard.




%\todo{Properties of the type system
%\begin{enumerate}
%\item Weakening and strengthening lemmas
%\item Substitution lemma
%\item Subject congruence 
%\item Subject reduction, for balanced environments
%\item Type safety (with appropriate definitions of error)
%\end{enumerate}
%}
